es:ES, P:(E).
(e':E. Dec(P(e')))
 (l:IdLnk, e:E. Dec(e':E. ((isrcv(e')) & lnk(e') = l & sender(e') = e & P(e')))) 

latex

Definitions	A, {T}, P  Q, x:A. B(x), Dec(P), A c B, x. t(x), P & Q, t  T, x(s), P  Q, , x:A. B(x), False
Lemmas	not wf, es-causle wf, decidable es-E-equal, decidable equal IdLnk, decidable and, decidable assert, decidable cand, es-sender wf, es-lnk wf, es-isrcv wf, assert wf, decidable existse-causle, es-sends-bound, event system wf, decidable wf, IdLnk wf, es-E wf